Inductive Id : Set := id : nat -> Id.